\begin{tabbing}
@$i$ \=Precondition for $a$(v)\+
\\[0ex]$P$ State(${\it ds}$) (v:$T$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)\+
\\[0ex]\& \=$\forall$$e$@$i$. kind($e$) $=$ locl($a$) $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$ \& $P$((state when $e$),val($e$))\+
\\[0ex]\& $\forall$$e$@$i$. $\exists$$e$$\leq$${\it e'}$.kind(${\it e'}$) $=$ locl($a$) $\vee$ ($\forall$$v$:$T$. $\neg$$P$(state after ${\it e'}$,$v$))
\\[0ex]\& (($\exists$$v$:$T$. $P$(es\_init(${\it es}$)($i$),$v$)) $\Rightarrow$ ($\exists$$e$:E. loc($e$) $=$ $i$))
\-\-
\end{tabbing}